Date: Wed, 5 Oct 88 9:56:39 WET DST
From: Brian Randell <B.Randell@newcastle.ac.uk>
Subject: Program Verification: The very idea

I have just finished reading, with great interest and enjoyment, an article by 
J.H. Fetzer with  the above title, which appeared in Comm ACM 31,9 (Sept. 88) 
pp. 1048-1063. 

In my opinion it is a very careful and lucid analysis of the dispute between,
e.g., DeMillo, Lipton and Perlis on the one hand, and Hoare on the other,
regarding the nature of programming and the significance of program
verification. Its abstract is as follows:

  The notion of program verification appears to trade on an equivocation. 
  Algorithms, as logical structures, are appropriate structures for deductive
  verification. Programs, as causal models of these structures, are not. The
  success of program verification as a generally applicable and completely 
  reliable method of guaranteeing program performance is not even a theoretical
  possibility.

The final chapter, entitled "Complexity and Reliability", is the one which most
explicitly relates to the interests of the RISKS readership but its
understanding requires a careful reading of much of the earlier part of the
paper. The final chapter, incidentally ends as follows:

  In maintaining that program verification cannot succeed as a generally
  applicable and completely reliable method for guaranteeing the performance of
  a program, DeMillo, Lipton and Perlis thus arrived at the right general 
  conclusion for the wrong specific reasons. Still, we are indebted to them for
  their efforts to clarify a conclusion whose potential consequences - not only
  for the community of computer science, but for the human race - cannot be
  overstated and had best be understood.

Brian Randell

Date: Tue, 29 Nov 88 07:11:44 -0500
From: leveson@electron.LCS.MIT.EDU
Subject: "Program Verification: The Very Idea", by J.H. Fetzer

In RISKS-7.61, Brian Randell recommended a paper by J.H. Fetzer in the
Communications of the ACM vol 31, no 9 (Sept. 88), pp. 1048-1063.  There has
been no reply in the RISKS Forum, and some people have apparently interpreted
this absence as everyone's agreement with Brian's view of the paper.  It should
be noted, however, that the paper has created great outrage among many in the
research community due to its misstatements and distortion of the goals of
formal verification, the seemingly low level of knowledge and understanding by
the author about formal verification (e.g., misstatements such as the
implication that it is only applicable to high-level languages and the lack of
references to the verification literature and work of the past 20 years), the
inclusion of inflammatory and unsupported statements (e.g., that the practice
of program verification somehow has serious negative consequences ``not only
for the community of computer science, but for the human race''), and the
general argument that deductive reasoning is not appropriate for computer
programs -- which has implications far beyond just formal verification.

Formal, mathematical approaches to system construction and analysis are
directly motivated by the concern to construct trustworthy systems -- systems
whose developers will be willing to stand before the public and take
responsibility for the consequences of their deployment.  As yet, this goal is
unrealized, but research in formal verification is a serious contribution
toward that goal and is both socially and scientifically responsible.  Serious
and well-informed discussion of the limitations to formal verification, and of
its strengths and defects relative to other responsible proposals for the
construction of trustworthy systems, is entirely appropriate and would, we are
sure, be welcomed by the supporters of formal verification.  In fact, many in
the field have themselves been the leaders of such discussion (e.g., see the
recent discussion by Avra Cohn, ``Correctness Properties of the Viper Block
Model'', Cambridge University, England, 1988, regarding her own verification of
the Viper microprocessor, and several papers in the book "Mathematical Logic
and Programming Languages" that was published on the occasion of C.A.R. Hoare
being named to the Royal Society).  However, ill-informed and irresponsible
attacks upon work that attempts to make computer science a socially-responsible
engineering endeavor do not seem to us to be useful or productive.

                      Mark Ardis, Software Engineering Institute
                      Victor Basili, University of Maryland
                      Daniel Craigen, I.P. Sharp
                      Susan Gerhart, MCC
                      Donald Good, Computational Logic Inc.
                      David Gries, Cornell University
                      Dick Kemmerer, University of California, Santa Barbara
                      Nancy Leveson, University of California, Irvine
                      John McHugh, Computational Logic Inc.
                      Peter Neumann, SRI International
                      Friedrich von Henke, SRI International

       [Other anticipated signatories were not available for final sign-off.]